\documentclass[11pt,a4paper]{article}

\usepackage{url,,}
\usepackage{graphicx}
\usepackage{hyperref}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{multirow}
\usepackage{listings}
\usepackage{fullpage}
\usepackage{fancyhdr,a4wide}
\usepackage{makeidx}
\usepackage{placeins}
%\usepackage[procnames,noindent]{lgrind}

\lstset{ %
language=VHDL,                % choose the language of the code
basicstyle=\footnotesize,       % the size of the fonts that are used for the code
showstringspaces=false,         % underline spaces within strings
%numbers=left,                   % where to put the line-numbers
%numberstyle=\footnotesize,      % the size of the fonts that are used for the line-numbers
%stepnumber=1,                   % the step between two line-numbers. If it's 1 each line will be numbered
%numbersep=5pt,                  % how far the line-numbers are from the code
%backgroundcolor=\color{white},  % choose the background color. You must add \usepackage{color}
showspaces=false,               % show spaces within strings adding particular underscores
showtabs=false,                 % show tabs within strings adding particular underscores
escapeinside={\%*}{*)}          % if you want to add a comment within your code
}

\begin{document}	

\begin{titlepage}

\thispagestyle{fancy}
\lhead{}
\chead{
\large{\textit{
Informatics and Mathematical Modelling\\
Technical University of Denmark}}}
\rhead{}
\rule{0pt}{50pt}
\vspace{3cm}

\begin{center}
 	\huge{\textbf{02241 : Robust Programming in .NET}}\\
 	\vspace{1cm}
 	\huge{Examination Project (DSB Railway Modeler)}\\
 	\vspace{1cm}
 	\huge{\textit{Final Report}}\\
 	\vspace{1cm}
 	\huge{Group \textit{06}}\\
\end{center}

\vspace{5cm}

\begin{flushright}
	\LARGE{Markku Eerola (s053739)}\\
	\vspace{0.3cm}
	\LARGE{Jakob Hommelhoff (s071312)}\\
\end{flushright}
\cfoot{\today}
\end{titlepage}

\newpage 
\tableofcontents

\newpage

\begin{abstract}
\centering
DSB wants a robust program that validates railway networks created from track listings and routes created from route listings. A robust program handles invalid inputs, and upon an internal error it terminates gracefully providing enough information for debugging. We have designed and implemented such a program using SPEC\#. The robustness is achieved using Design by Contract enforced by SPEC\# system and defensive programming. The resulting program performs in a robust fashion in respect to different inputs. We also conclude that SPEC\# is a good idea, and a welcome addition to the tools of the trade once it is ready, but it still requires a lot of work before it can be called mature.
\end{abstract}


\section{Introduction}
This document is the final report on the examination project on the IMM course 02241 Robust Programming in .NET. The goal of the project was to design and implement a railway modeler for the purposes of DSB. The modeler was to take as input track listings and route listings and then verify the correctness of the listings as well as model and validate the railway network and the routes based on the listings. The modeler was to be implemented with robust programming methods using SPEC\# language. \\

In the remainder of the introduction we will present the concept of robust programming and the SPEC\# programming system. In chapter 2 we analyse the requirements for the project. In chapter 3 we present our design and in chapter 4, how we implemented it. Chapter 4 contains discussion about the results and the project in general. It also concludes the report. \\

\subsection{Robust Programming}
Writing error-free code is extremely difficult. The more complex the program, the more fragile it is likely to be and the more errors it is likely to contain. The errors could be \textit{compile-time errors}, occurring as a result of syntactical mismatch of the program with the language specifications, or \textit{run-time program errors}, occurring as a result of e.g. a null pointer accessing data or an array index being negative -- these are impossible to recover from and the program has to notify the user and terminate, or \textit{run-time user errors}, occurring as a result of unrecognised user input, or they could be \textit{run-time exceptions}, internal error situations which can be handled by the program to some extent. \\

Robust programs deal with the last three kinds of errors occurring at run-time without abnormal output or unspecified behaviour. A program is robust, if it handles any bad inputs in a reasonable way, and upon an internal error it terminates gracefully providing enough information for debugging. According to Bishop \cite{bishop} a robust program adheres to the following four principles of robust programming:

\begin{itemize}
	\item \textbf{Paranoia.} One should assume, that anyone using ones program or library routine will attempt to break it. Also when calling another functions, one should check that the call succeeds. Most importantly one should not trust oneself, and always program defensively so that problems in ones own code can be dealt with quickly.
	\item \textbf{Stupidity.} One should assume that everyone is an idiot, oneself included, and cannot read any documentation. Thus any input, no matter how absurd, should be handled in a reasonable fashion. Any error messages or codes should be self-explanatory, detailed and unambigious.
	\item \textbf{Dangerous Implements.} Anything ones routines expect to remain consistent across calls is a ``dangerous implement'' and should be hidden from users.
	\item \textbf{Can't Happen.} One should think about (and implement) how to handle seemingly impossible situations. Those situations are most often not impossible, only highly unlikely. Repeated modifications to the the code, for example, can cause inconsistent effects and lead to ``impossible'' situations.
\end{itemize}

In general defensive programming is a very useful method of robust programming and it should definitely be used without exception in any program or library routine where abnormal output or unspecified behaviour might have serious consequences -- be it a matter of data security, material security or safety of human beings. As a good (warning) example of serious consequences we can take the fate of Ariane 5 Flight 501 \cite{ariane}. Long story short, a malfunction in the control software ended in destruction of US\$370 million worth of equipment. \\

Another useful method is Design by Contract (DBC), first introduced by Meyer in 1992 \cite{meyer}. From what DBC introduces, the things that interest us the most here are the pre- and postconditions and invariants. Preconditions of a method state the conditions which must hold at the time of a method being called. These conditions can refer to states of the object before executing the method, to states of objects reachable from the state before executing the method, and to the arguments of the method. Meeting the preconditions is the callers responsibility. Postconditions of a method state the conditions which must hold immediately after the execution of the method. These conditions can refer to states of the object before and after executing the method, to states of objects reachable from the state of the object before and after executing, to the arguments of the method, and to the result of the method. Meeting the postconditions is the responsibility of the method. Invariants state what has to hold during the whole execution of the system \textit{while the system is stable}. It is possible, and also necessary when e.g. creating objects -- an invariant stating that a variable is not null can not hold before the variable is initialized, to specify when the system is not stable, or in other words, when the object which the invariant targets is \textit{exposed}. \\

The problem with DBC is that for the conditions and invariants to be useful one has to be able to control the caller and make sure that the caller honors them. If one has this control, DBC is really useful to guarantee that methods work as they are designed, thus rooting out errors. Defensive programming on the other hand works as it is even when one can not trust the caller. These two methods do not rule each other out, either. They can be used together, using DBC in a program whenever the caller can be controlled and covering other parts of the program by programming defensively. \\

\subsection{SPEC\#}

The SPEC\# programming system is developed by Microsoft as a tool of writing robust programs. The system is integrated on the existing .NET platform to make it more easily adoptable. It consists of SPEC\# language, which is an extension to the object oriented .NET programming language C\#, a SPEC\# compiler, which has been fully integrated into MS Visual Studio, and an automatic static program verifier codenamed Boogie. \cite{barnett} \\

SPEC\# adds annotations that allow the programmer to distinguish between possibly-null and non-null expressions. It also adds annotations for DBC: The programmer can specify pre- and postconditions to methods as well as object invariants. \\

The Spec\# programming system includes both compile-time and run-time checking. The SPEC\# compiler statically enforces non-null types, turns pre- and postconditions into inlined code for run-time contract checking, records the contracts as metadata for consumption by analysis tools, and adds a new method to each class to check object invariants at run-time. The compile-time checking means that many errors that might otherwise have caused unexpected behavior or abnormal exits can be caught during compilation. Not only does this decrease the amount of errors in the end product but it also increases the efficiency of the program because things that can be checked during compilation do not need to be checked again run-time. \\

The static program verifier Boogie constructs the SPEC\# program in its own intermediate language, BoogiePL, and through ,any transformations generates logical verification conditions from it. It then uses an automatic theorem prover to analyze the verification conditions to prove the correctness of the program, or find errors. Boogie will catch some errors during compile-time which would go undetected in the SPEC\# run-time checks, such as checking whether an object is exposed before its fields are updated. \\

While the additions made to C\# by SPEC\# sound good and are definitely welcome they do not automatically mean that using SPEC\# will increase robustness. The language cannot e.g. eradicate null-dereference errors on its own. The tool is only as good as its user. If the programmer does not exploit the new features using the language does not guarantee correctness. Still, it is obvious that having the tools will make it easier to promote correctness especially within a larger project. Example: Alice writes her methods using the pre- and post-conditions to ensure that when Bob calls her methods he is forced to do so with correct arguments. Because of this Bob cannot cause unexpected behavior within Alice's code. Without the means of control SPEC\# provides, the only thing Alice could do to attempt avoiding errors is program defensively and adhere to the four principles of robust programming. \\

\section{Analysis}
This section contains the analysis of the system that DSB wish to be provided with. The section is further structured into three subsections. The first one contains a description and analysis of how the railway network can be modeled. The second one consists of the specifications for the train routes. The third section touches upon possible extension of the system in a way that would allow it to take into account route timings. \\

\subsection{Modeling the tracks}
The engineers at DSB have decided that the new system of railways should have three kinds of tracks. These three tracks are supposed to be the building blocks for the entire network. These tracks are:

\begin{itemize}
\item \textit{Straight Track} This track connects two stations. A straight track between stations A and B indicates a direct connection between these stations.
\item \textit{Switch Track} This track forms a switch between three stations. Any train running on this track from one end would have the possibility of switching path to one of the two stations on the other end. It is assumed that the 'node' in the center of the switch track is not a station.
\item \textit{End Track} An end track is simply a track which starts from one station and ends without connecting to any other station. The end track would always connect a station to an end point, which is not a station.
\end{itemize}

Having said this, we need to specify a way by which DSB could model its network of stations and the kinds of tracks connecting them. This is done using a simple grammar for track listings. Assuming the identifier is a unique way to identify a station, the basic keywords in the grammar are:

\begin{itemize}
\item \verb,STAT, followed by the name of the station and an identifier, indicates a station.
\item \verb,CONN, followed by two identifiers, indicates a connection between the identifiers. A connection directly refers to a straight track (if both the identifiers are stations, and none is a `node').
\item \verb,END, followed by an identifier of a station, indicates that one connection to the identifier ends. An end keyword directly refers to an end track.
\end{itemize}

\noindent As we can see, the straight and end tracks can be directly constructed using the keywords \verb,STAT, and \verb,CONN,. A switch track cannot be directly constructed using one keyword, but is constructed using more than one of these keywords. A simple example for switch tracks is shown here,

\begin{verbatim}
STAT Hellerup h
STAT Lyngby l
STAT Klampenborg k
CONN h b
CONN b l
CONN b k
\end{verbatim}

Here, we have three stations specified by the \verb'STAT' statements. The \verb,CONN, statements use the stations, and also introduce an identifier `b' which is not a station. It can be clearly seen that the specification above represents a switch track, where `b' is the `node' which connects the three stations. \\

\noindent To brief it up, there are only three kinds of tracks that are used to define the entire track network. These tracks are specified using the grammar described above. \\

\subsection{Defining train routes}

Once the track network is defined, different routes can be mapped on it. This is done using a simple grammar for route listings. The keyword for a route is \verb,ROUTE, and it is followed by a list of identifiers (station or 'node') and \verb,STOP, keywords. The identifiers mark the route and the stops mark the positions where trains are supposed to stop. \\

A simple example of a route specification: \\

\verb,ROUTE h b STOP l STOP, \\

This means that a train first goes from `h' to `b' and stops. Then it continues from `b' to `l' and stops again. Such routes would be considered valid only if there are stations or nodes with the identifiers given in the route, and that they are adjacently connected to each other. The system would check the validity of the routes in the specification, and notify about faults in the specification. \\
 
Some more conditions on the routes are:

\begin{itemize}
\item Trains can change directions only when they are stopped. In the simple case, this means that if a train is wanted to go back on some portion of the path it has already travelled, it has to be indicated in the route listing with a \verb,STOP,. 
\item Switch tracks have a sense of direction in the branches. This means that, using tree terminology, a train can travel from parent to child or child to parent, and never child to child without stopping at the parent first and changing direction. \\
\end{itemize}


\subsection{Extension: Simulation of trains}
\label{simulation}
Once the specification of the train routes is done, we could simulate the trains on the tracks by specifying exact timings. For all the points in the routes of trains, the exact time of the train arriving at that point, and then departing from that point, could be specified. This is illustrated by the following example: \\

\verb,ROUTE h 0 34 b STOP 55 71 l STOP, \\

The above example can be read as: Train starts at `h' at time 0, reaches `b' at time 34 and stops there. Then it continues starting at time 55 and stops at `l' at time 71. \\

Once such a specification is provided for all the routes, the system would be able to check if there are any collisions occuring between any two trains. If a collision is detected, the system could recommend changing the timings in the routes. \\


\section{Design}
% XXX Revise! XXX
The system design is object-oriented. Originally all the functionalities of the system were planned to revolve around three classes representing different types of tracks. These track types were straight tracks, switch tracks and end tracks. During the course of the project we found this inconvenient and clumsy, and decided to take a different direction instead. The classes we ended up using are presented in figure \ref{classdiagram}. \\ 

\begin{figure}[htb]
	\centering
		\includegraphics{./images/RailwayModelerClassdiagram.jpg}
	\caption{The class diagram of the Railway Modeler}	\label{classdiagram}
\end{figure}

The RailwayModeler class has the main method and it orchestrates the functionality of the program by controlling the network through the RailwayNetwork class and handling the input using the InputHandler class. The InputHandler validates the input files. The RailwayNetwork class keeps track of the network, which consists of \textit{Nodes}, \textit{Stations} and \textit{Endtracks}. \\

The Nodes are the base of the network, and in practice this means that the network is a graph-like structure where the Nodes are the vertices and the connections between Nodes are the edges. These connections are referred to as \textit{parents} and \textit{children}. A Node must have at most one parent and at most two children. A Node can have at most one Station. If a Node does not have a station, it is the middle-point of a switch track, and must have two children -- in our design we do not allow stationeless nodes otherwise. The Nodes have a string identifier, which will have the value of one of the identifiers from the track listing, references to the Node's parent and children, and a reference to a Station. Connections between adjacent Nodes correspond to the straight tracks of the original design idea while the stationless Nodes along with the connections to its parent and children correspond to the switch tracks. \\

The Stations contain a string identifier, in the same way as the Nodes, and a string containing the name of the station. The Station class also contains the method for validating station entries in the track listing. \\

The Endtracks contain a string identifier, in the same way as the Nodes, and a reference to a Station. The Endtrack class contains the method for validating the end entries in the track listing. The Endtracks correspond to the end tracks of the original design idea. \\

The Connection class contains the method which is used for validating the connection entries in the track listing. \\

The Route class handles the route information and route validation. \\

The track and route listings are given to the program in plain text files. We have set a constraint on the track listings which have to be followed, or our program decides the resulting track network is invalid: Once the first connection is described it defines which direction the parent-child flow must follow. This means that if the track listing has contained \verb,CONN a b, then \verb,CONN c b, is not acceptable. The flow of the track, so to speak, must be in the same direction all the time. \\

If parts of the track listing file are invalid our program will still generate a network from the valid lines. If the resulting network is invalid, then the user must try with a fixed listing, otherwise the user can start validating routes. A track network is invalid if:

\begin{itemize}
	\item There is a node with no parent and no children.
	\item There is a node with only one parent and no children, or one child and no parent, or exactly one of both, and it doesn't have a station.
	\item There is a node with two children and no parent.
	\item There is a node with two children and one parent and it has a station.
	\item There is a node which has either only a child or a parent, and the station of the node doesn't have an endtrack.
\end{itemize}

To generalize: A valid network must consist of complete straight, switch and endtracks -- or the ideas of those, since we will use nodes, stations and end tracks instead -- and there must be no open ends. All nodes not centers of a switch track must have a station.

\FloatBarrier
\section{Implementation}

SPEC\# method contracts have been used throughout the program to ensure that use of methods is well defined.
Especially Pre- and post- conditions have played an important part in the implementation. Method constraints that have a high risk of being violated due to errornous input are set to throw exceptions, which in turn are caught by the envoker, allowing for a meaningful errormessage to be presented to the user. Also the SPEC\# specific non-null types were found to be useful in implementing a robust solution. \\

Typed collections have been used where possible. The Node collection of the Network class is implemented as a typed dictionary of Nodes, with the key being the Id of the node. This makes it impossible to add nodes or stations with the same Id as other nodes or stations. \\

We have implemented extensive checking logic for validating both file input as well as the interaction between railway network components. A well structured class hierarchy also contributes in the overall robustness of the program. \\

We have aspired to use object oriented priciples for distributing knowledge and responsibility among classes.
A good example of the principle of low coupling and high cohesion can be seen in the validation of individual network elements. The Station class is responsible for validating input lines that start with 'STAT' and the Connection class responsible for validating input of the 'CONN' type. \\

The program is structured around the singleton RailwayNetwork class, which makes use of most of the other classes. The Util class contains functions that are not part of the business logic. Due to a bug, the string!.Split() method had to be forced to use the C\# legacy variant string.Split(). Also found in the the Util class is a method for printing network information to the console. \\

\section{Discussion}

Looking back, we had a rocky road with our project. As if personal setbacks and group organizational changes which both caused us to miss the initial deadline, and even to struggle with the extension, were not enough, we had a lot of problems with the tools we were supposed to use. We assume that these problems were largely caused by the immature state of SPEC\# system. Since it is still in development the team has not been able to smoothen all the bumps yet. The top three of worst problems with SPEC\# integrated to Visual Studio 2005 we encountered and had to put up with on regular basis were:

\begin{enumerate}
	\item VS 2005 terminates without any error messages for no apparent reason. Often this manifested as the tool freezing completely and demanding manual intervention in the form of killing the process tree. This kind of behaviour seems ironic in a tool that is supposed to promote robustness.
	\item VS 2005 becomes sluggish to use. This does not manifest itself with any of the environments that come built-in with the tool, only with the SPEC\# extension.
	\item The tool is slow to refresh changes and insists that an error that has been fixed still persists, and refuses to compile the design. This may happen as easily when a simple typing mistake is corrected as when an incorrect line is completely removed. The tool refuses to compile until the code file has been closed and reopened. Doing this often leads to the top one problem: VS terminates without explanation.
\end{enumerate}

We would be willing to accept the explanation that our installation was faulty if we had not heard other groups complain about the same issues. We have no other choice but to draw the conclusion, that while the idea behind SPEC\# is sound, and the system is definitely a welcome tool once it is more mature, as it is now it brings more problems than it solves. Granted, even as it is now, the system brings with it the benefits of static checks, but it is much easier to just rely on defensive programming and adherence to the four principles of robust programming. \\

During the course of the project we became more familiar with different concepts involved in robust programming. Many we were somewhat familiar with from the beginning, but repetition is always a good thing. We had not however heard of SPEC\# before. \\

Unfortunately we eventually had to drop many of the aspects we had originally intended to implement. We intended to maximize the use of invariants but did not get them to work in time. For this reason we decided to drop the invariants and use method contracts and manual checking instead. We also had to scrap the extension ideas we had about simulating trains on the network. \\

We will, however, briefly describe our ideas about the train simulations here in the discussion: \\

We planned, that separate routes complete with timing constraints as described in the section \ref{simulation} would be added for each train i.e. each route description in the route listing would have referred to one train. The program would then have, after validating the routes, compared the routes together to find out if multiple routes referred to same points in the track network. When encountering overlapping routes the program would use the time stamps to see when different trains would be located in these overlapping points. The program would then, if possible, retime the routes so, that no collisions on the overlappings would remain. This would be done both by increasing and decreasing the timestamps. The amounts by which the stamps would be changed would depend on the time unit chosen for the simulation. Decreasing the time would have to have a lower limit than increasing, since the trains can only travel so fast. The trains which arrive to the points first or spend least time on the overlapping part of the routes would be given first priority in the retiming. If the program would be unable to remove some collisions it would still remove what it can, and then inform the user about the changes it made to the routes and which collisions still remain. \\

Even with our shortcomings, such as failing to add invariants, we are pretty satisfied in how we managed to make our program robust in respect to inputs. All the invalid inputs we tried were caught without any unknown exceptions or meaningless error messages. We recognice the fact that we should have used unit testing to verify this, and had time allowed it we would have, but we had to rely on empiric testing only. Although lacking in some of the SPEC\# features, we feel that we have constructed a program that meets the requirements in the specification, as they are derived in the analysis. \\


\bibliographystyle{plain}
\bibliography{final}
\end{document}